# The three-valued Legendre symbol from squares

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-legendre-symbol/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-legendre-symbol-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Modulo 7 the symbol on 0,1,2,3,4,5,6 is respectively 0,1,1,-1,1,-1,-1.

Complete square-table classification at odd prime 7, without Euler criterion or Jacobi extension.





## Givens and symbols


- calc


- G1 — p=7; L(a)=(a/7), with a first normalized to 0 through 6.


- L(a) — Legendre value (a/7)
- p — fixed odd prime 7





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus. Assume the complete trial-division primality criterion.
- mko_definition · cited — Normalize a modulo odd prime p first. If p divides a, (a/p)=0; otherwise the value is 1 for a nonzero square class and−1 for another nonzero class. Classification uses a complete nonzero square table or root witness, not a prematurely assumed Euler criterion. Modulus2 and composite moduli are outside this node domain, and a few multiplicativity samples do not prove a general result. · mko-legendre-symbol





## Main derivation

S01 · impliesBefore

p=7

After

7\text{ odd prime};\quad L(a)=L(a\bmod7)

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

2 does not divide 7 and 3^2>7, qualifying odd primality, then bind the symbol to residue classes.



S02 · impliesBefore

x=1,2,3,4,5,6

After

\begin{array}{c|rrrrrr}x&1&2&3&4&5&6\\\hline x^2\bmod7&1&4&2&2&4&1\end{array}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Compute all six squares directly without Euler criterion.



S03 · impliesBefore

a\equiv0\pmod7

After

L(a)=0

Conditions: none

Rule: mko_definition · Uses: G1, S01

Leaf basis: mko_definition

Handle zero first rather than assigning +1 because zero is a square.



S04 · impliesBefore

a\bmod7\in\{1,2,4\}

After

L(1)=L(2)=L(4)=1

Conditions: none

Rule: calc · Uses: G1, S02, S03

Leaf basis: calc

The table has nonzero roots, respectively 1,3,2, giving +1.



S05 · impliesBefore

a\bmod7\in\{3,5,6\}

After

L(3)=L(5)=L(6)=-1

Conditions: none

Rule: calc · Uses: G1, S02, S03, S04

Leaf basis: calc

These nonzero classes are absent from all square values, giving -1.



S06 · impliesBefore

a=0,1,2,3,4,5,6

After

L(a)=0,1,1,-1,1,-1,-1\text{ respectively}

Conditions: none

Rule: mko_definition · Uses: G1, S03, S04, S05

Leaf basis: mko_definition

The three branches form the full symbol table on all seven classes.



S07 · impliesBefore

-4\equiv3,\quad9\equiv2,\quad14\equiv0\pmod7

After

L(-4)=-1,\quad L(9)=1,\quad L(14)=0

Conditions: none

Rule: calc · Uses: G1, S06

Leaf basis: calc

Use the same table for a negative input, large positive input and zero class, showing normalization first.



S08 · impliesBefore

L(2)=1,\quad L(3)=-1,\quad2\cdot3=6

After

L(6)=-1=L(2)L(3)\text{ in this instance}

Conditions: none

Rule: calc · Uses: G1, S06, S07

Leaf basis: calc

One multiplicativity instance can be checked, but it is not the general theorem.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S06, S07 — The classification used no half-power congruence, avoiding a circular Euler-based definition.
- S07 · premise_audit · G1, S06 — 9's integer-square appearance is not the classification method; residue 2 has root 3.
- S06 · premise_audit · G1, S03, S04, S05 — The zero,+1,-1 branches are disjoint and classify each class once.
- S05 · premise_audit · G1, S02, S03, S04 — Testing only x=1,2 would not prove absence.
- S04 · premise_audit · G1, S02, S03 — Roots are witnesses; the complete table also certifies absence for other classes.
- S03 · premise_audit · G1, S01 — a=14 is the zero class and has value 0.
- S02 · premise_audit · G1, S01 — The complete table supports both root witnesses and nonsquare absence.
- S01 · premise_audit · G1 — The denominator in the symbol is not division; a may be negative while p is an odd prime.





## Error controls and negative controls

Zero firstAfter normalization test p dividing a before nonzero square/nonsquare classification.

No circularityThe symbol comes from complete squares, not its later Euler criterion.


- (14/7)=1 because zero is a square. → reject — The zero branch specifically returns 0.
- The same table directly defines Legendre (a/8). → reject — 8 is not an odd prime and is outside this symbol's domain.
- One multiplication example proves general multiplicativity. → reject — It checks only the pair 2,3 and not the universal statement.





## Result and limitations

Modulo 7 the symbol on 0,1,2,3,4,5,6 is respectively 0,1,1,-1,1,-1,-1.







## Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bf6613da5aa41f52a17e16f75b5886f4fb614337c244c624146c4ed59148ad74
- original source SHA-256: 90e7d3c68f6ec4970520bf9ddc0f5ddc1a6905fc6b9958fe26e324b623ca2856
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-legendre-symbol-01.json)